COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST RW ε WORLD
C00007 ENDMK
C⊗;
declare INDCONST RW ε WORLD;
declare INDVAR w w1 w2 w3 ε WORLD;
declare INDVAR m n m1 m2 m3 n1 n2 n3 ε NATNUM;

declare INDCONST W1 W2 W12 ε PERSON;
declare INDVAR p p0 p1 p2 ε PERSON;

declare PREDCONST A(WORLD,WORLD,PERSON,NATNUM);

declare INDVAR c c1 c2 c3 c4 ε COLORS;
declare INDCONST W B ε COLORS;

declare OPCONST color(PERSON,WORLD) = COLORS;

axiom reflex:	∀w p m.A(w,w,p,m);;

axiom transitive:	∀w1 w2 w3 p m.(A(w1,w2,p,m) ∧ A(w2,w3,p,m) ⊃ A(w1,w3,p,m));;

axiom w12:	∀w1 w2 m.(A(w1,w2,W1,m) ∨ A(w1,w2,W2,m) ⊃ A(w1,w2,W12,m))
;;

axiom color:	¬(W=B)
		∀c.(c=W ∨ c=B)
;;

axiom rw:	color(W1,RW) = W ∧ color(W2,RW) = W;;

axiom initial:	∀c w.(A(RW,w,W12,0) ⊃
	(c=W ∨ color(W2,w)=W ⊃ ∃w1.(A(w,w1,W1,0) ∧ color(W1,w1) = c)) ∧
	(c=W ∨ color(W1,w)=W ⊃ ∃w1.(A(w,w1,W2,0) ∧ color(W2,w1) = c)))

	∀w w1.(A(RW,w,W12,0) ∧ A(w,w1,W1,0) ⊃ color(W2,w1) = color(W2,w))
	∀w w1.(A(RW,w,W12,0) ∧ A(w,w1,W2,0) ⊃ color(W1,w1) = color(W1,w))
;;

axiom king:	∀w.(A(RW,w,W12,0) ⊃ color(W1,w)=W ∨ color(W2,w)=W);;

axiom w2lw1k:	∀w.(A(RW,w,W12,1) ≡ A(RW,w,W12,0)
		∧ ∀w1.(A(w,w1,W2,0) ⊃
			(∀w2.(A(w1,w2,W1,0) ⊃ color(W1,w2)=color(W1,w1)) ≡
			∀w2.(A(w,w2,W1,0) ⊃ color(W1,w2)=color(W1,w)))))

	∀w1 w2.(A(w1,w2,W1,1) ≡ A(w1,w2,W1,0) ∧ A(w1,w2,W12,1))
	∀w1 w2.(A(w1,w2,W2,1) ≡ A(w1,w2,W2,0) ∧ A(w1,w2,W12,1))
;;

axiom elwek:	∀w.(A(RW,w,W12,1) ≡ A(RW,w,W12,0) ∧
( ∀w1.(A(w,w1,W1,0) ⊃ ∀w2.(A(w1,w2,W2,0) ⊃ color(W2,w2)=color(W2,w1))) ∨
  ∀w1.(A(w,w1,W1,0) ⊃ ∃w2.(A(w1,w2,W2,0) ∧ ¬(color(W2,w2)=color(W2,w1))))) ∧
( ∀w1.(A(w,w1,W2,0) ⊃ ∀w2.(A(w1,w2,W1,0) ⊃ color(W1,w2)=color(W1,w1))) ∨
  ∀w1.(A(w,w1,W2,0) ⊃ ∃w2.(A(w1,w2,W1,0) ∧ ¬(color(W1,w2)=color(W1,w1))))))

	∀w1 w2.(A(w1,w2,W1,1) ≡ A(w1,w2,W1,0) ∧ A(w1,w2,W12,1))
	∀w1 w2.(A(w1,w2,W2,1) ≡ A(w1,w2,W2,0) ∧ A(w1,w2,W12,1))
;;

axiom elweka:	∀w.(A(RW,w,W12,1) ≡ A(RW,w,W12,0) ∧
	∀p.(∀w1.(A(w,w1,p,0) ⊃ color(p,w1)=color(p,w)) ≡ ∀w1.(A(RW,w1,p,0)
⊃ color(p,w1)=color(p,RW))))

	∀w1 w2.(A(w1,w2,W1,1) ≡ A(w1,w2,W1,0) ∧ A(w1,w2,W12,1))
	∀w1 w2.(A(w1,w2,W2,1) ≡ A(w1,w2,W2,0) ∧ A(w1,w2,W12,1))
;;
COMMENT : elweka is the current candidate for what happens when everyone learns
whether everyone knows the color of his spot.  The sentence starting ∀p.
says that p knows the color of his spot in w iff he knows it in RW. :

mark 3;
axiom suzman:	∀w2.(A(RW,w2,W12,1) ≡ A(RW,w2,W12,0)
			 ∧ (∃w3.(A(w2,w3,W1,0)
				  ∧ ¬(color(W1,w3) = color(W1,w2)))
			 ∨ ∀w3.(A(w2,w3,W1,0)
				  ⊃ color(W1,w3) = color(W1,w2)))

			 ∧ (∃w3.(A(w2,w3,W2,0)
				  ∧ ¬(color(W2,w3) = color(W2,w2)))
			 ∨ ∀w3.(A(w2,w3,W2,0)
				  ⊃ color(W2,w3) = color(W2,w2))))
;;

axiom suzman2:	∀w2.(A(RW,w2,W12,1) ≡ A(RW,w2,W12,0)
			 ∧ (∃w3.(A(w2,w3,W1,0)
				  ∧ ¬(color(W1,w3) = color(W1,w2)))
			 ∨ ∀w3.(A(w2,w3,W1,0)
				  ⊃ color(W1,w3) = color(W1,w2)))

			 ∧ (∃w3.(A(w2,w3,W2,0)
				  ∧ ¬(color(W2,w3) = color(W2,w2)))
			 ∨ ∀w3.(A(w2,w3,W2,0)
				  ⊃ color(W2,w3) = color(W2,w2))))
;;

mark 4;

declare PREDCONST true(PROPOSITION,WORLD,NATNUM);
declare OPCONST knows(PERSON,CONCEPT) = PROPOSITION;